An Algebraic Preservation Theorem for Aleph-Zero Categorical Quantified Constraint Satisfaction

23 p. -- An extended abstract of this work appears in the proceedings of the 2012 ACM/IEEE Symposium on Logic in Computer Science

Beyond Q-Resolution and Prenex Form: a Proof System for Quantified Constraint Satisfaction

We consider the quanti fied constraint satisfaction problem (QCSP) which is to decide, given a structure and a first-order sentence (not assumed here to be in prenex form) built from conjunction and quanti fication, whether or not the sentence is true on the structure. We present a proof system for certifying the falsity of QCSP instances and develop its basic theory; for instance, we provide an algorithmic interpretation of its behavior. Our proof system places the established Q-resolution proof system in a broader context, and also allows us to derive QCSP tractability results.

A prioritised fuzzy constraint satisfaction approach to model agent negotiation for railway scheduling

With the recent regulatory reforms in a number of countries, railways resources are no longer managed by a single party but are distributed among different stakeholders. To facilitate the operation of train services, a train service provider (SP) has to negotiate with the infrastructure provider (IP) for a train schedule and the associated track access charge. This paper models the SP and IP as software agents and the negotiation as a prioritized fuzzy constraint satisfaction (PFCS) problem. Computer simulations have been conducted to demonstrate the effects on the train schedule when the SP has different optimization criteria. The results show that by assigning different priorities on the fuzzy constraints, agents can represent SPs with different operational objectives.

The use of object oriented modelling and simulation tools in constraint satisfaction for embodiment design

The software package Dymola, which implements the new, vendor-independent standard modelling language Modelica, exemplifies the emerging generation of object-oriented modelling and simulation tools. This paper shows how, in addition to its simulation capabilities, it may be used as an embodiment design tool, to size automatically a design assembled from a library of generic parametric components. The example used is a miniature model aircraft diesel engine. To this end, the component classes contain extra algebraic equations calculating the overload factor (or its reciprocal, the safety factor) for all the different modes of failure, such as buckling or tensile yield. Thus the simulation results contain the maximum overload or minimum safety factor for each failure mode along with the critical instant and the device state at which it occurs. The Dymola "Initial Conditions Calculation" function, controlled by a simple software script, may then be used to perform automatic component sizing. Each component is minimised in mass, subject to a chosen safety factor against failure, over a given operating cycle. Whilst the example is in the realm of mechanical design, it must be emphasised that the approach is equally applicable to the electrical or mechatronic domains, indeed to any design problem requiring numerical constraint satisfaction.

Compositional model repositories via dynamic constraint satisfaction with order-of-magnitude preferences

J. Keppens and Q. Shen. Compositional model repositories via dynamic constraint satisfaction with order-of-magnitude preferences. Journal of Artificial Intelligence Research, 21:499-550, 2004.

Identifying sources of global contention in constraint satisfaction search

Much work has been done on learning from failure in search to boost solving of combinatorial problems, such as clause-learning and clause-weighting in boolean satisfiability (SAT), nogood and explanation-based learning, and constraint weighting in constraint satisfaction problems (CSPs). Many of the top solvers in SAT use clause learning to good effect. A similar approach (nogood learning) has not had as large an impact in CSPs. Constraint weighting is a less fine-grained approach where the information learnt gives an approximation as to which variables may be the sources of greatest contention. In this work we present two methods for learning from search using restarts, in order to identify these critical variables prior to solving. Both methods are based on the conflict-directed heuristic (weighted-degree heuristic) introduced by Boussemart et al. and are aimed at producing a better-informed version of the heuristic by gathering information through restarting and probing of the search space prior to solving, while minimizing the overhead of these restarts. We further examine the impact of different sampling strategies and different measurements of contention, and assess different restarting strategies for the heuristic. Finally, two applications for constraint weighting are considered in detail: dynamic constraint satisfaction problems and unary resource scheduling problems.

Image segmentation based on multi-scan constraint satisfaction neural network

A novel image segmentation method based on a constraint satisfaction neural network (CSNN) is presented. The new method uses CSNN-based relaxation but with a modified scanning scheme of the image. The pixels are visited with more distant intervals and wider neighborhoods in the first level of the algorithm. The intervals between pixels and their neighborhoods are reduced in the following stages of the algorithm. This method contributes to the formation of more regular segments rapidly and consistently. A cluster validity index to determine the number of segments is also added to complete the proposed method into a fully automatic unsupervised segmentation scheme. The results are compared quantitatively by means of a novel segmentation evaluation criterion. The results are promising.